\begin{tabbing}
$e$ leaks $x$ to ${\it e'}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$a$:Atom1.\+
\\[0ex]$\neg$loc($e$) $>>$ $a$
\\[0ex]\& $\neg$state when $e$$\backslash\backslash$$x$:state@loc($e$)$\backslash\backslash$$x$$>>$$a$
\\[0ex]\& $\neg$$e$ receives $a$
\\[0ex]\& isrcv(${\it e'}$) \& sender(${\it e'}$) $=$ $e$ \& val(${\it e'}$):valtype(${\it e'}$)$>>$$a$
\-
\end{tabbing}